perm filename PCHECK.LAP[CHE,WD]1 blob
sn#018930 filedate 1973-01-05 generic text, type T, neo UTF8
(LAP DELETEPROP SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 1.)
TAG1 (HRRZ@ 1. 0. P)
(JUMPE 1. TAG3)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CAME 1. -1. P)
(JRST 0. TAG8)
(HRRZ@ 1. 0. P)
(CALL 1. (E CDDR))
(HRRM@ 1. 0. P)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG2)
TAG8 (HRRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP GETGET SUBR)
(PUSH P 1.)
(PUSH P 2.)
(HRRZ@ 1. 1.)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -1. P)
(JUMPE 1. TAG3)
(MOVE 2. -2. P)
(HLRZ@ 1. -1. P)
(CALL 2. (E SEEKPROP))
(MOVEM 1. 0. P)
(JUMPE 1. TAG8)
(JRST 0. TAG2)
TAG8 (HRRZ@ 1. -1. P)
(HRRZ@ 1. 1.)
(MOVEM 1. -1. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP INITPROP SUBR)
(PUSH P 2.)
(HRRZ@ 2. 1.)
(EXCH 1. 0. P)
(CALL 2. (E CONS))
(MOVE 2. 3.)
(CALL 2. (E XCONS))
(HRRM@ 1. 0. P)
(POP P 1.)
(POPJ P)
NIL
(LAP SEEKPROP SUBR)
(PUSH P 1.)
(PUSH P 2.)
(MOVE 1. 2.)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 2. (E GETL))
(PUSH P 1.)
(JUMPE 1. TAG2)
(MOVE 1. 0. P)
(JRST 0. TAG1)
TAG2 (MOVEI 1. (QUOTE NIL))
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP AE FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(MOVEI 2. (QUOTE AND))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (FIRST ARG IS NOT AN AND)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 2. -1. P)
(MOVE 1. 0. P)
(CALL 2. (E ANDELIM1))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE AE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP AI FSUBR)
(PUSH P 1.)
(CALL 1. (E WFFLIST))
(CALL 1. (E CONJOIN))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE AI))
(CALL 2. (E CONS))
(EXCH 1. -1. P)
(CALL 1. (E ASSLIST))
(CALL 1. (E UNION))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP ALT FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E ALT1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (LINES ARE NOT ALTERNATIVES)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE ALT))
(CALL 2. (E CONS))
(CALL 1. (E NCONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ASS FSUBR)
(MOVEI 2. (QUOTE ASS))
(PUSH P 1.)
(CALL 2. (E XCONS))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(MOVEM 1. -1. P)
(CALL 0. (E NEXTLINE))
(CALL 1. (E NCONS))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(JCALL 3. (E ADDLINE))
NIL
(LAP BS FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E MAKECONSES))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E BOUNDSUBST))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE BS))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP DED FSUBR)
(PUSH P 1.)
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NOTHING TO CONCLUDE)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 1. 0. P)
(CALL 1. (E WFFLIST))
(CALL 1. (E CONJOIN))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(CALL 1. (E WFFPART))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE IMPLIES))
(CALL 2. (E XCONS))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE DED))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(HRRZ@ 2. -2. P)
(CALL 2. (E SETDIF))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP DEF FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NAMES MUST BE ATOMS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. 0. P)
(MOVEI 1. (QUOTE SETQ))
(CALL 2. (E CONS))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE DEF))
(CALL 2. (E CONS))
(PUSH P 1.)
(CALL 0. (E NEXTLINE))
(CALL 1. (E NCONS))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP DNE FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(CALL 1. (E DOUBLENEG))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO DOUBLE NEGATIVE)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE DNE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP DNI FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE NOT))
(CALL 2. (E XCONS))
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE NOT))
(CALL 2. (E XCONS))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE DNI))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP EG FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 2. 0. P)
(CALL 2. (E EXGEN1))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE EG))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP ELIM FSUBR)
(PUSH P 1.)
(CALL 1. (E CADR))
(CALL 1. (E WFFPART))
(PUSH P 1.)
(MOVEI 2. (QUOTE SETQ))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO DEFINITION)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E CADR))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E WFFPART))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(CALL 3. (E SUBST))
(MOVE 2. -2. P)
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE ELIM))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E SETDIF))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP EQE FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(MOVEI 2. (QUOTE EQUIVALENT))
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO EQUIVALENCE)))
(CALL 1. (E ERREND))
TAG5 (MOVEI 2. (QUOTE 2.))
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG8)
(HRRZ@ 1. 0. P)
(CALL 1. (E REVERSE))
(JRST 0. TAG7)
TAG8 (HRRZ@ 1. 0. P)
TAG7 (MOVEI 2. (QUOTE IMPLIES))
(MOVEM 1. 0. P)
(CALL 2. (E XCONS))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE EQE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP EQI FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E EQI1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (ARE NOT EQUIVALENT)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE EQI))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ES FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 2. 0. P)
(CALL 2. (E SPECALL))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE ES))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP IFE FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E IFE1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO IF /- THEN /- ELSE EXPRESSION)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE IFE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP IFI FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E IFI1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NEED IMPLICATIONS WITH OPPOSITE ANTECEDENTS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE IFI))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP LC FSUBR)
(PUSH P 1.)
(CALL 1. (E LAMEXP))
(CALL 1. (E NCONS))
(MOVE 2. 0. P)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE EQUAL))
(CALL 2. (E XCONS))
(POP P 2.)
(PUSH P 1.)
(MOVEI 1. (QUOTE LC))
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(POP P 1.)
(JCALL 3. (E ADDLINE))
NIL
(LAP MP FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E MP1))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (CANNOT MODUS PONENS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE MP))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP NE FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E NOTELIM))
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO CONTRADICTION)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. 0. P)
(MOVEI 1. (QUOTE NE))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(MOVEI 1. (QUOTE FALSE))
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP NI FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(CALL 1. (E NOTINTRO))
(MOVEM 1. 0. P)
(CALL 1. (E VALID))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO IMPLIES FALSE)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. -1. P)
(MOVEI 1. (QUOTE NI))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP OE FSUBR)
(PUSH P 1.)
(JUMPE 1. TAG7)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG5)
TAG7 (MOVEI 1. (QUOTE (NEED AT LEAST TWO ARGS)))
(CALL 1. (E ERREND))
TAG5 (HLRZ@ 1. 0. P)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E WFFLIST))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E ORELIM1))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE OE))
(CALL 2. (E CONS))
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 1. (E ASSLIST))
(CALL 1. (E UNION))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP OI FSUBR)
(PUSH P 1.)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -3. P)
(JUMPN 1. TAG7)
(MOVE 1. 0. P)
(JUMPN 1. TAG10)
(MOVEI 1. (QUOTE (NO VALID PROPOSITION)))
(CALL 1. (E ERREND))
(JRST 0. TAG9)
TAG10 (JRST 0. TAG2)
TAG9
TAG7 (HLRZ@ 1. -3. P)
(CALL 1. (E NUMBERP))
(JUMPE 1. TAG14)
(MOVE 1. 0. P)
(JUMPN 1. TAG16)
(HLRZ@ 1. -3. P)
(MOVEM 1. 0. P)
TAG16
TAG14 (HLRZ@ 1. -3. P)
(CALL 1. (E NUMBERP))
(JUMPE 1. TAG19)
(HLRZ@ 1. -3. P)
(CALL 1. (E WFFPART))
(MOVE 2. -1. P)
(CALL 2. (E CONS))
(MOVEM 1. -1. P)
(JRST 0. TAG18)
TAG19 (MOVE 2. -1. P)
(HLRZ@ 1. -3. P)
(CALL 2. (E CONS))
(MOVEM 1. -1. P)
TAG18 (HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. -1. P)
(JUMPN 1. TAG23)
(HLRZ@ 1. -1. P)
(JRST 0. TAG22)
TAG23 (MOVE 1. -1. P)
(CALL 1. (E REVERSE))
(MOVEI 2. (QUOTE OR))
(CALL 2. (E XCONS))
TAG22 (MOVE 2. -2. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE OI))
(CALL 2. (E CONS))
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP REP FSUBR)
(PUSH P 1.)
(CALL 1. (E CADR))
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ISEQUIVALENCE))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO EQUATION)))
(CALL 1. (E ERREND))
TAG5 (MOVEI 2. (QUOTE 2.))
(HRRZ@ 1. -1. P)
(CALL 1. (E CADR))
(CALL 2. (E EQUAL))
(JUMPE 1. TAG8)
(HRRZ@ 1. 0. P)
(CALL 1. (E REVERSE))
(JRST 0. TAG7)
TAG8 (HRRZ@ 1. 0. P)
TAG7 (MOVEM 1. 0. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E WFFPART))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(CALL 3. (E SUBST))
(MOVE 2. -2. P)
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE REP))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -3. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP REPL FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 4. -1. P)
(HRRZ@ 4. 4.)
(HLRZ@ 4. 4.)
(MOVEI 3. (QUOTE T))
(MOVE 2. 1.)
(POP P 1.)
(CALL 4. (E REPEITHER))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE REPL))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP REPR FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 4. -1. P)
(HRRZ@ 4. 4.)
(HLRZ@ 4. 4.)
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(POP P 1.)
(CALL 4. (E REPEITHER))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE REPR))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ASSPART))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E UNION2))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(SUB P (C 0. 0. 1. 1.))
(JCALL 3. (E ADDLINE))
NIL
(LAP TAUT FSUBR)
(PUSH P 1.)
(HRRZ@ 1. 1.)
(CALL 1. (E WFFLIST))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(CALL 1. (E NCONS))
(MOVE 4. 1.)
(POP P 3.)
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE NIL))
(CALL 4. (E TH1))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (DOES NOT FOLLOW)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. 0. P)
(MOVEI 1. (QUOTE TAUT))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(CALL 1. (E ASSLIST))
(CALL 1. (E UNION))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP UG FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(CALL 1. (E ASSPART))
(HRRZ@ 2. -1. P)
(PUSH P 2.)
(PUSH P 1.)
TAG1 (MOVE 1. -1. P)
(JUMPE 1. TAG5)
(HLRZ@ 1. -1. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (ILLEGAL ARGUMENT)))
(CALL 1. (E ERREND))
TAG2 (HLRZ@ 4. -1. P)
(MOVE 3. 4.)
(MOVE 2. 0. P)
(MOVE 1. -2. P)
(CALL 4. (E UNGEN))
(MOVEM 1. -2. P)
(JRST 0. TAG4)
TAG3 (HLRZ@ 4. -1. P)
(HRRZ@ 4. 4.)
(HRRZ@ 4. 4.)
(HLRZ@ 4. 4.)
(HLRZ@ 3. -1. P)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(MOVE 2. 0. P)
(MOVE 1. -2. P)
(CALL 4. (E UNGEN))
(MOVEM 1. -2. P)
TAG4 (HRRZ@ 1. -1. P)
(MOVEM 1. -1. P)
(JRST 0. TAG1)
TAG5 (MOVE 2. -3. P)
(MOVEI 1. (QUOTE UG))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -4. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(MOVE 1. -2. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP US FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(HRRZ@ 2. 0. P)
(CALL 2. (E SPECALL))
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE US))
(CALL 2. (E CONS))
(PUSH P 1.)
(HLRZ@ 1. -2. P)
(CALL 1. (E ASSPART))
(MOVE 3. 1.)
(POP P 2.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP USEAX FSUBR)
(PUSH P 1.)
(MOVEI 2. (QUOTE AXIOM))
(HLRZ@ 1. 1.)
(CALL 2. (E GET))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO SUCH AXIOM)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 2. -2. P)
(MOVE 1. -1. P)
(CALL 2. (E SPECALL))
(MOVE 2. -2. P)
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE USEAX))
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP USESCHM FSUBR)
(PUSH P 1.)
(MOVEI 2. (QUOTE SCHEMA))
(HLRZ@ 1. 1.)
(CALL 2. (E GET))
(PUSH P 1.)
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (IS NOT SCHEMA)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 3. 0. P)
(HLRZ@ 3. 3.)
(HLRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 3. (E PROPSUBST))
(CALL 1. (E LAMEXP))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE USESCHM))
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP USETHM FSUBR)
(PUSH P 1.)
(MOVEI 2. (QUOTE THEOREM))
(HLRZ@ 1. 1.)
(CALL 2. (E GET))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO SUCH THEOREM)))
(CALL 1. (E ERREND))
TAG5 (HRRZ@ 2. -2. P)
(MOVE 1. -1. P)
(CALL 2. (E SPECALL))
(MOVE 2. -2. P)
(MOVEM 1. 0. P)
(MOVEI 1. (QUOTE USETHM))
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 3. (E ADDLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP BT FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(JUMPN 1. TAG5)
(CALL 0. (E CURLINE))
(MOVEI 2. (QUOTE 1.))
(CALL 2. (E *DIF))
(JRST 0. TAG4)
TAG5 (HLRZ@ 1. -1. P)
TAG4 (MOVEM 1. -1. P)
(CALL 0. (E CURTEXT))
(MOVEM 1. 0. P)
(CALL 0. (E CURLINE))
(MOVE 2. -1. P)
(CALL 2. (E *LESS))
(JUMPN 1. TAG12)
(MOVEI 2. (QUOTE 0.))
(MOVE 1. -1. P)
(CALL 2. (E *LESS))
(JUMPE 1. TAG10)
TAG12 (MOVEI 1. (QUOTE (NON EXISTANT LINE)))
(CALL 1. (E ERREND))
TAG10 (MOVEI 2. (QUOTE 0.))
(MOVE 1. -1. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG14)
(CALL 0. (E CURPROOF))
(MOVEI 3. (QUOTE PROOF))
(MOVEI 2. (QUOTE NIL))
(CALL 3. (E PUTPROP))
(JRST 0. TAG13)
TAG14 (MOVEI 2. (QUOTE 1.))
(MOVE 1. -1. P)
(CALL 2. (E *DIF))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E NTHCDR))
(HLLZS@ 0. 1.)
(CALL 0. (E CURPROOF))
(MOVEI 3. (QUOTE PROOF))
(MOVE 2. 0. P)
(CALL 3. (E PUTPROP))
TAG13 (CALL 0. (E CURPROOF))
(CALL 1. (E INITPROOF))
(CALL 0. (E SHOWCURLINE))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP FINDL FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HRRZ@ 1. -3. P)
(JUMPE 1. TAG6)
(HRRZ@ 2. -3. P)
(HLRZ@ 2. 2.)
(JRST 0. TAG5)
TAG6 (CALL 0. (E CURPROOF))
(MOVE 2. 1.)
TAG5 (MOVEM 2. 0. P)
(MOVEI 2. (QUOTE PROOF))
(MOVE 1. 0. P)
(CALL 2. (E GET))
(MOVEM 1. -1. P)
TAG1 (MOVE 1. -1. P)
(JUMPE 1. TAG3)
(HLRZ@ 2. -1. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(MOVE 1. -2. P)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG14)
(HLRZ@ 1. -1. P)
(CALL 1. (E SHOWLINE))
TAG14 (HRRZ@ 1. -1. P)
(MOVEM 1. -1. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP GIVEAX FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NON ATOMIC AXIOM NAME)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. (SPECIAL AXIOMS))
(HLRZ@ 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG8)
(HLRZ@ 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. (SPECIAL AXIOMS))
(CALL 2. (E *APPEND))
(MOVEM 1. (SPECIAL AXIOMS))
TAG8 (MOVEI 3. (QUOTE AXIOM))
(HRRZ@ 2. 0. P)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 0. P)
(CALL 3. (E PUTPROP))
(MOVE 1. (SPECIAL *PRINT))
(JUMPE 1. TAG11)
(HLRZ@ 1. 0. P)
(CALL 1. (E SHOWAXIOM))
TAG11 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP GIVESCHM FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NON ATOMIC SCHEMA NAME)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. (SPECIAL SCHEMAS))
(HLRZ@ 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG8)
(HLRZ@ 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. (SPECIAL SCHEMAS))
(CALL 2. (E *APPEND))
(MOVEM 1. (SPECIAL SCHEMAS))
TAG8 (MOVEI 3. (QUOTE SCHEMA))
(HRRZ@ 2. 0. P)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 0. P)
(CALL 3. (E PUTPROP))
(MOVE 1. (SPECIAL *PRINT))
(JUMPE 1. TAG11)
(HLRZ@ 1. 0. P)
(CALL 1. (E SHOWSCHEMA))
TAG11 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP INVENTORY SUBR)
(MOVE 1. (SPECIAL AXIOMS))
(JUMPE 1. TAG5)
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE AXIOMS))
(CALL 1. (E PRINT))
(MOVE 1. (SPECIAL AXIOMS))
(CALL 1. (E PRINL))
TAG5 (MOVE 1. (SPECIAL SCHEMAS))
(JUMPE 1. TAG12)
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE SCHEMAS))
(CALL 1. (E PRINT))
(MOVE 1. (SPECIAL SCHEMAS))
(CALL 1. (E PRINL))
TAG12 (MOVE 1. (SPECIAL PROOFS))
(JUMPE 1. TAG19)
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE PROOFS))
(CALL 1. (E PRINT))
(MOVE 1. (SPECIAL PROOFS))
(CALL 1. (E PRINL))
TAG19 (MOVE 1. (SPECIAL THEOREMS))
(JUMPE 1. TAG26)
(CALL 0. (E TERPRI))
(MOVEI 1. (QUOTE THEOREMS))
(CALL 1. (E PRINT))
(MOVE 1. (SPECIAL THEOREMS))
(CALL 1. (E PRINL))
TAG26 (MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP MAKETHM FSUBR)
(PUSH P 1.)
(PUSH P 1.)
(PUSH P 1.)
(CALL 1. (E CADR))
(PUSH P 1.)
(HLRZ@ 1. -1. P)
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(HRRZ@ 1. 1.)
(JUMPE 1. TAG2)
(HRRZ@ 3. -2. P)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(JRST 0. TAG1)
TAG2 (CALL 0. (E CURPROOF))
(MOVE 3. 1.)
TAG1 (MOVE 2. -1. P)
(POP P 1.)
(SUB P (C 0. 0. 4. 4.))
(JCALL 3. (E MAKETHEOREM1))
NIL
(LAP ONDD SUBR)
(CALL 0. (E INITSTANCHARSET))
(MOVE 1. (SPECIAL DDWIDTH))
(MOVEM 1. (SPECIAL CONSOLEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP ONIII SUBR)
(CALL 0. (E INITSTANCHARSET))
(MOVE 1. (SPECIAL IIIWIDTH))
(MOVEM 1. (SPECIAL CONSOLEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP ONIMLAC SUBR)
(CALL 0. (E INITSTANCHARSET))
(MOVE 1. (SPECIAL IMLACWIDTH))
(MOVEM 1. (SPECIAL CONSOLEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP ONTTY SUBR)
(CALL 0. (E INITTTYCHARSET))
(MOVE 1. (SPECIAL TTYWIDTH))
(MOVEM 1. (SPECIAL CONSOLEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP PROOF FSUBR)
(PUSH P 1.)
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO NAME GIVEN)))
(CALL 1. (E ERREND))
TAG5 (HLRZ@ 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG8)
(MOVEI 1. (QUOTE (NON ATOMIC PROOF NAME)))
(CALL 1. (E ERREND))
TAG8 (HLRZ@ 1. 0. P)
(CALL 1. (E INITPROOF))
(MOVE 1. (SPECIAL *PRINT))
(JUMPE 1. TAG11)
(CALL 0. (E SHOWCURLINE))
TAG11 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP REDO FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(PUSH P 1.)
(HRRZ@ 1. -5. P)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(POP P 2.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG7)
(MOVEI 1. (QUOTE (CANNOT REDO)))
(CALL 1. (E ERREND))
TAG7 (HRRZ@ 2. -4. P)
(HLRZ@ 2. 2.)
(HLRZ@ 1. -4. P)
(CALL 2. (E CONS))
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE 1.))
(MOVEM 1. 0. P)
(HLRZ@ 1. -4. P)
(CALL 2. (E *PLUS))
(MOVEM 1. -1. P)
(CALL 0. (E CURLINE))
(MOVEI 2. (QUOTE 1.))
(CALL 2. (E *PLUS))
(MOVEM 1. -2. P)
TAG1 (MOVE 1. -1. P)
(CAMN 1. -2. P)
(JRST 0. TAG4)
(MOVE 1. -1. P)
(CALL 1. (E BYPART))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
(MOVEM 1. -3. P)
(MOVE 1. -1. P)
(CALL 1. (E BYPART))
(MOVE 2. -3. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG2)
(MOVE 1. -3. P)
(CALL 1. (E *EVAL))
(CALL 0. (E CURLINE))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(MOVE 2. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG2 (MOVEI 2. (QUOTE 1.))
(MOVE 1. -1. P)
(CALL 2. (E *PLUS))
(MOVEM 1. -1. P)
(JRST 0. TAG1)
TAG4 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 5. 5.))
(POPJ P)
NIL
(LAP RESTOREALL FSUBR)
(JSP 6. SPECBIND)
(0. 0. (SPECIAL *PRINT))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(MOVE 1. (SPECIAL *FILEPRINT))
(JUMPE 1. TAG11)
(MOVEI 1. (QUOTE T))
(MOVEM 1. (SPECIAL *PRINT))
TAG11 (MOVEI 1. (QUOTE DSK))
(MOVEM 1. 0. P)
TAG1 (MOVE 1. -2. P)
(JUMPE 1. TAG6)
(HLRZ@ 1. -2. P)
(MOVEM 1. -1. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. -1. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. -1. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (NOT FILE OR DEVICE NAME)))
(CALL 1. (E ERREND))
TAG2 (MOVE 1. -1. P)
(CALL 1. (E NCONS))
(MOVEI 3. (QUOTE NIL))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 3. (E READIN))
(JRST 0. TAG5)
TAG3 (HRRZ@ 2. -1. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(CALL 2. (E CONS))
(MOVEM 1. -1. P)
(JRST 0. TAG2)
TAG4 (HRRZ@ 1. -1. P)
(HLRZ@ 1. 1.)
(MOVEM 1. 0. P)
(JRST 0. TAG5)
TAG5 (HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG6 (CALL 0. (E INVENTORY))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(JRST 0. SPECSTR)
NIL
(LAP SAVEALL FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE DSK) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -2. P)
(JUMPN 1. TAG9)
(MOVEI 1. (QUOTE (DEVICE BUT NO FILE)))
(CALL 1. (E ERREND))
TAG9 (HLRZ@ 1. -2. P)
(MOVEM 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (NOT FILE SPECIFIER)))
(CALL 1. (E ERREND))
TAG2 (HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(HRRZ@ 2. -2. P)
(MOVEM 1. -1. P)
(MOVEM 2. -2. P)
(JRST 0. TAG1)
TAG3 (HRRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG4 (MOVE 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(CALL 15. (E OUTPUT))
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE T))
(CALL 2. (E OUTC))
(MOVE 1. (SPECIAL FILEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVE 2. (SPECIAL AXIOMS))
(MOVEI 1. (QUOTE SAVEAXIOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE SAVESCHEMA))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL PROOFS))
(MOVEI 1. (QUOTE SAVEPROOF))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL THEOREMS))
(MOVEI 1. (QUOTE SAVETHEOREM))
(CALL 2. (E MAPC))
(MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE NIL))
(CALL 2. (E OUTC))
(CALL 0. (E INVENTORY))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP SAVECOMS FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE DSK) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -2. P)
(JUMPN 1. TAG9)
(MOVEI 1. (QUOTE (NO FILE SPECIFIED)))
(CALL 1. (E ERREND))
TAG9 (HLRZ@ 1. -2. P)
(MOVEM 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (NOT FILE SPECIFIER)))
(CALL 1. (E ERREND))
TAG2 (HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(HRRZ@ 2. -2. P)
(MOVEM 1. -1. P)
(MOVEM 2. -2. P)
(JRST 0. TAG1)
TAG3 (HRRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG4 (MOVE 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(CALL 15. (E OUTPUT))
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE T))
(CALL 2. (E OUTC))
(MOVE 1. (SPECIAL FILEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVE 2. (SPECIAL AXIOMS))
(MOVEI 1. (QUOTE SAVEAXCOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE SAVESCHMCOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL PROOFS))
(MOVEI 1. (QUOTE SAVEPRFCOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL THEOREMS))
(MOVEI 1. (QUOTE SAVETHMCOM))
(CALL 2. (E MAPC))
(MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE NIL))
(CALL 2. (E OUTC))
(CALL 0. (E INVENTORY))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP SHOW FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -3. P)
(JUMPN 1. TAG12)
(CALL 0. (E CURPROOF))
(CALL 1. (E SHOWPROOF))
(JRST 0. TAG8)
TAG12
TAG2 (MOVE 1. -3. P)
(JUMPE 1. TAG7)
(HLRZ@ 1. -3. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG6)
(HLRZ@ 1. -3. P)
(CALL 1. (E NUMBERP))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE IMAGE))
(HLRZ@ 1. -3. P)
(CALL 2. (E GETGET))
(MOVEM 1. -2. P)
(JUMPN 1. TAG20)
(MOVEI 1. (QUOTE (NOTHING TO SHOW)))
(CALL 1. (E ERREND))
TAG20 (MOVEI 1. (QUOTE ((CADR TEM) (CAR THINGS))))
(CALL 1. (E *EVAL))
TAG3 (HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG2)
TAG4 (HLRZ@ 1. -3. P)
(HRRZ@ 2. -3. P)
(MOVEM 1. 0. P)
(MOVEM 2. -3. P)
(JUMPE 2. TAG25)
(HLRZ@ 1. 2.)
(CALL 1. (E NUMBERP))
(JUMPN 1. TAG23)
TAG25 (MOVE 1. 0. P)
(MOVEM 1. -1. P)
(JRST 0. TAG22)
TAG23 (HLRZ@ 1. -3. P)
(HRRZ@ 2. -3. P)
(MOVEM 1. -1. P)
(MOVEM 2. -3. P)
TAG22
TAG5 (MOVE 2. -1. P)
(MOVE 1. 0. P)
(CALL 2. (E *GREAT))
(JUMPN 1. TAG7)
(MOVE 1. 0. P)
(CALL 1. (E GETLINE))
(CALL 1. (E SHOWLINE))
(MOVEI 2. (QUOTE 1.))
(MOVE 1. 0. P)
(CALL 2. (E *PLUS))
(MOVEM 1. 0. P)
(JRST 0. TAG5)
TAG6 (MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG35)
(MOVEI 1. (QUOTE (NEED NAME OR FILE SPEC)))
(CALL 1. (E ERREND))
TAG35 (HLRZ@ 1. -3. P)
(CALL 1. (E CADR))
(CALL 15. (E OUTPUT))
(MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE T))
(CALL 2. (E OUTC))
(HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG1)
TAG7 (MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE NIL))
(CALL 2. (E OUTC))
(MOVEI 1. (QUOTE NIL))
TAG8 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP SHOWALL FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE DSK) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -2. P)
(JUMPN 1. TAG9)
(MOVEI 1. (QUOTE (NO FILE SPECIFIED)))
(CALL 1. (E ERREND))
TAG9 (HLRZ@ 1. -2. P)
(MOVEM 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG4)
(MOVEI 2. (QUOTE QUOTE))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. 0. P)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (NOT FILE SPECIFIER)))
(CALL 1. (E ERREND))
TAG2 (HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(HRRZ@ 2. -2. P)
(MOVEM 1. -1. P)
(MOVEM 2. -2. P)
(JRST 0. TAG1)
TAG3 (HRRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E CONS))
(MOVEM 1. 0. P)
TAG4 (MOVE 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. -1. P)
(CALL 2. (E XCONS))
(CALL 15. (E OUTPUT))
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE T))
(CALL 2. (E OUTC))
(MOVE 1. (SPECIAL FILEWIDTH))
(CALL 1. (E LINELENGTH))
(MOVE 2. (SPECIAL AXIOMS))
(MOVEI 1. (QUOTE SHOWAXIOM))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE SHOWSCHEMA))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL PROOFS))
(MOVEI 1. (QUOTE SHOWPROOF))
(CALL 2. (E MAPC))
(MOVE 2. (SPECIAL THEOREMS))
(MOVEI 1. (QUOTE SHOWTHEOREM))
(CALL 2. (E MAPC))
(MOVEI 2. (QUOTE T))
(MOVEI 1. (QUOTE NIL))
(CALL 2. (E OUTC))
(CALL 0. (E INVENTORY))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP SSEX FSUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(JUMPN 1. TAG8)
(CALL 0. (E CURPROOF))
(JRST 0. TAG7)
TAG8 (HLRZ@ 1. -3. P)
TAG7 (MOVEI 2. (QUOTE (PROOF)))
(MOVEM 1. -1. P)
(CALL 2. (E GETL))
(MOVEM 1. -2. P)
(JUMPN 1. TAG13)
(MOVEI 1. (QUOTE (NO PROOF BY THAT NAME)))
(CALL 1. (E ERREND))
TAG13 (HRRZ@ 1. -2. P)
(HLRZ@ 1. 1.)
(MOVEM 1. -2. P)
(MOVEI 1. (QUOTE PROOF))
(CALL 1. (E PRINT))
(MOVE 1. -1. P)
(CALL 1. (E PRINS))
TAG1 (MOVE 1. -2. P)
(JUMPE 1. TAG5)
(HLRZ@ 1. -2. P)
(MOVEM 1. 0. P)
(CALL 0. (E TERPRI))
(HLRZ@ 1. 0. P)
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE //))
(CALL 1. (E PRINC))
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(PUSH P 1.)
(CALL 0. (E CURCOL))
(MOVEI 3. (QUOTE 0.))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E PRINTSUBEXPR))
(HRRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(CALL 1. (E FLATSIZE))
(MOVEI 2. (QUOTE 6.))
(CALL 2. (E *PLUS))
(PUSH P 1.)
(CALL 0. (E CHRCT))
(POP P 2.)
(CALL 2. (E *LESS))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE //))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE BY))
(CALL 1. (E PRINS))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADR))
(CALL 1. (E PRINS))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(JUMPE 1. TAG19)
(MOVEI 1. (QUOTE ASS))
(CALL 1. (E PRINS))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(CALL 1. (E PRIN1))
TAG19
TAG2 (HRRZ@ 1. -2. P)
(MOVEM 1. -2. P)
(JRST 0. TAG1)
TAG3 (CALL 0. (E TERPRI))
(MOVEI 2. (QUOTE 4.))
(MOVEI 1. (QUOTE //))
(CALL 2. (E PRINTN))
(MOVEI 1. (QUOTE BY))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE //))
(CALL 1. (E PRINC))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADR))
(PUSH P 1.)
(CALL 0. (E CURCOL))
(MOVEI 3. (QUOTE 0.))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E PRINTSUBEXPR))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(JUMPE 1. TAG2)
(CALL 0. (E TERPRI))
(MOVEI 2. (QUOTE 4.))
(MOVEI 1. (QUOTE //))
(CALL 2. (E PRINTN))
(MOVEI 1. (QUOTE ASS))
(CALL 1. (E PRINC))
(MOVEI 1. (QUOTE //))
(CALL 1. (E PRINC))
(HRRZ@ 1. 0. P)
(CALL 1. (E CADDR))
(CALL 1. (E PRINS))
(JRST 0. TAG2)
TAG5 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP ADDLINE SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(CALL 0. (E CURPROOF))
(PUSH P 1.)
(PUSH P (C 0. 0. TAG4 0.))
(CALL 0. (E CURTEXT))
(PUSH P 1.)
(CALL 0. (E CURLINE))
(MOVEI 2. (QUOTE 1.))
(CALL 2. (E *PLUS))
(PUSH P 1.)
(MOVE 1. -4. P)
(CALL 1. (E NCONS))
(MOVE 2. -5. P)
(CALL 2. (E XCONS))
(MOVE 2. -6. P)
(CALL 2. (E XCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(CALL 1. (E NCONS))
(PUSH P 1.)
(MOVNI 6. 2.)
(JCALL 14. (E NCONC))
TAG4 (MOVEI 3. (QUOTE PROOF))
(MOVE 2. 1.)
(POP P 1.)
(CALL 3. (E PUTPROP))
(MOVEI 2. (QUOTE 1.))
(MOVE 1. (SPECIAL CURLIN))
(CALL 2. (E *PLUS))
(MOVEM 1. (SPECIAL CURLIN))
(CALL 0. (E CURLINE))
(MOVEI 3. (QUOTE NEWNAM))
(MOVE 2. 1.)
(MOVEI 1. (QUOTE /@))
(CALL 3. (E PUTPROP))
(MOVE 1. (SPECIAL *PRINT))
(JUMPE 1. TAG6)
(CALL 0. (E SHOWCURLINE))
TAG6 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP ADDAXIOM FSUBR)
(PUSH P 1.)
(MOVEI 3. (QUOTE AXIOM))
(HRRZ@ 2. 1.)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 1.)
(CALL 3. (E PUTPROP))
(MOVE 2. (SPECIAL AXIOMS))
(HLRZ@ 1. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. (SPECIAL AXIOMS))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ADDSCHEMA FSUBR)
(PUSH P 1.)
(MOVEI 3. (QUOTE SCHEMA))
(HRRZ@ 2. 1.)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 1.)
(CALL 3. (E PUTPROP))
(MOVE 2. (SPECIAL SCHEMAS))
(HLRZ@ 1. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ADDTHEOREM FSUBR)
(PUSH P 1.)
(MOVEI 3. (QUOTE THEOREM))
(HRRZ@ 2. 1.)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 1.)
(CALL 3. (E PUTPROP))
(MOVE 2. (SPECIAL THEOREMS))
(HLRZ@ 1. 0. P)
(CALL 2. (E CONS))
(MOVEM 1. (SPECIAL THEOREMS))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ALPHAPART SUBR)
(PUSH P 1.)
(CALL 1. (E EXPLODE))
(CALL 1. (E REVERSE))
(PUSH P 1.)
TAG1 (HLRZ@ 1. 0. P)
(CALL 1. (E NUMBERP))
(JUMPN 1. TAG6)
(MOVE 1. 0. P)
(CALL 1. (E REVERSE))
(CALL 1. (E READLIST))
(JRST 0. TAG2)
TAG6 (HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG2 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ALLVARS SUBR)
(MOVEI 2. (QUOTE NIL))
(JCALL 2. (E ALLVARS1))
NIL
(LAP ALLVARS1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. -1. P)
(CALL 1. (E ISVAR))
(JUMPE 1. TAG4)
(MOVE 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG6)
(MOVE 1. 0. P)
(JRST 0. TAG5)
TAG6 (MOVE 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E CONS))
TAG5 (JRST 0. TAG3)
TAG4 (MOVE 1. 0. P)
TAG3 (JRST 0. TAG1)
TAG2 (MOVE 2. 0. P)
(HRRZ@ 1. -1. P)
(CALL 2. (E ALLVARSL))
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ALLVARSL SUBR)
(PUSH P 1.)
(PUSH P 2.)
(JUMPN 1. TAG2)
(MOVE 1. 2.)
(JRST 0. TAG1)
TAG2 (HLRZ@ 1. -1. P)
(MOVE 2. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -2. P)
(CALL 2. (E ALLVARSL))
(MOVE 2. 1.)
(POP P 1.)
(CALL 2. (E ALLVARS1))
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ALT1 SUBR)
(PUSH P 2.)
(PUSH P 1.)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ)))
(CALL 3. (E INST))
(POP P 2.)
(EXCH 1. 0. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) QQQ)))
(CALL 3. (E INST))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG2)
(MOVEI 2. (QUOTE QQQ))
(MOVE 1. -1. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG2 (MOVE 1. 0. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG3)
(MOVEI 2. (QUOTE QQQ))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE INVALID))
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ANDELIM1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(HRRZ@ 1. 1.)
(CALL 1. (E LENGTH))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(MOVEI 2. (QUOTE AND))
(HLRZ@ 1. -3. P)
(CALL 2. (E NEQ))
(JUMPE 1. TAG6)
(MOVEI 1. (QUOTE (FIRST ARG IS NOT AN AND)))
(CALL 1. (E ERREND))
TAG6
TAG1 (MOVE 1. -2. P)
(JUMPN 1. TAG8)
(MOVE 1. 0. P)
(CALL 1. (E REVERSE))
(CALL 1. (E CONJOIN))
(JRST 0. TAG2)
TAG8 (MOVE 2. -1. P)
(HLRZ@ 1. -2. P)
(CALL 2. (E *GREAT))
(JUMPE 1. TAG11)
(MOVEI 1. (QUOTE (TOO FEW CONJUNCTS)))
(CALL 1. (E ERREND))
TAG11 (HLRZ@ 2. -2. P)
(HRRZ@ 1. -3. P)
(CALL 2. (E NTHELT))
(MOVE 2. 0. P)
(CALL 2. (E CONS))
(HRRZ@ 2. -2. P)
(MOVEM 1. 0. P)
(MOVEM 2. -2. P)
(JRST 0. TAG1)
TAG2 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP ASSLIST SUBR)
(MOVE 2. 1.)
(MOVEI 1. (QUOTE ASSPART))
(JCALL 2. (E MAPCAR))
NIL
(LAP ASSOCR SUBR)
(PUSH P 1.)
(PUSH P 2.)
TAG1 (MOVE 1. 0. P)
(JUMPE 1. TAG3)
(HLRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(CAME 1. -1. P)
(JRST 0. TAG8)
(HLRZ@ 1. 0. P)
(JRST 0. TAG2)
TAG8 (HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
TAG2 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP ASSPART SUBR)
(CALL 1. (E GETLINE))
(JCALL 1. (E CADDDR))
NIL
(LAP BINAND SUBR)
(PUSH P 1.)
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE (AND TRUE TRUE)))
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. 1.)
(JUMPN 1. TAG4)
(MOVEI 1. (QUOTE TRUE))
(CALL 1. (E NCONS))
(HLRZ@ 2. 0. P)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE AND))
(CALL 2. (E XCONS))
(JRST 0. TAG1)
TAG4 (HRRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG6)
(MOVE 2. 0. P)
(MOVEI 1. (QUOTE AND))
(CALL 2. (E CONS))
(JRST 0. TAG1)
TAG6 (HLRZ@ 1. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E BINAND))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE AND))
(CALL 2. (E XCONS))
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP BINOR SUBR)
(PUSH P 1.)
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE (OR FALSE FALSE)))
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. 1.)
(JUMPN 1. TAG4)
(MOVEI 1. (QUOTE FALSE))
(CALL 1. (E NCONS))
(HLRZ@ 2. 0. P)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE OR))
(CALL 2. (E XCONS))
(JRST 0. TAG1)
TAG4 (HRRZ@ 1. 0. P)
(HRRZ@ 1. 1.)
(JUMPN 1. TAG6)
(MOVE 2. 0. P)
(MOVEI 1. (QUOTE OR))
(CALL 2. (E CONS))
(JRST 0. TAG1)
TAG6 (HLRZ@ 1. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E BINOR))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 2. (QUOTE OR))
(CALL 2. (E XCONS))
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP BYPART SUBR)
(CALL 1. (E GETLINE))
(JCALL 1. (E CADDR))
NIL
(LAP BOUNDSUBST SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(CALL 1. (E ATOM))
(JUMPN 1. TAG1)
(HLRZ@ 1. -3. P)
(HLRZ@ 1. 1.)
(CALL 1. (E ISQUANT))
(JUMPN 1. TAG2)
(MOVE 3. -1. P)
(MOVE 2. -2. P)
(MOVE 1. -3. P)
(CALL 3. (E BOUNDSUBSTL))
(JRST 0. TAG3)
TAG1 (MOVE 1. -3. P)
(CALL 1. (E ISCONST))
(JUMPE 1. TAG9)
(MOVE 1. -3. P)
(JRST 0. TAG3)
TAG9 (MOVE 2. -1. P)
(MOVE 1. -3. P)
(CALL 2. (E ASSOC))
(MOVEM 1. 0. P)
(JUMPE 1. TAG11)
(HRRZ@ 1. 1.)
(JRST 0. TAG3)
TAG11 (MOVE 2. -1. P)
(MOVE 1. -3. P)
(CALL 2. (E ASSOCR))
(MOVEM 1. 0. P)
(JUMPE 1. TAG15)
(MOVEI 1. (QUOTE (FREE VARIABLE CAPTURE)))
(CALL 1. (E ERREND))
TAG15 (MOVE 1. -3. P)
(JRST 0. TAG3)
TAG2 (MOVE 2. -2. P)
(HLRZ@ 1. -3. P)
(CALL 1. (E CADR))
(CALL 2. (E ASSOC))
(MOVEM 1. 0. P)
(JUMPE 1. TAG19)
(HRRZ@ 2. 1.)
(JRST 0. TAG18)
TAG19 (HLRZ@ 2. -3. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
TAG18 (MOVEM 2. 0. P)
(MOVE 2. -1. P)
(MOVE 1. 0. P)
(CALL 2. (E ASSOCR))
(JUMPE 1. TAG25)
(MOVEI 1. (QUOTE (BOUND VARIABLE CAPTURE)))
(CALL 1. (E ERREND))
TAG25 (MOVE 1. 0. P)
(CALL 1. (E NCONS))
(HLRZ@ 2. -3. P)
(HLRZ@ 2. 2.)
(CALL 2. (E XCONS))
(MOVE 2. 0. P)
(PUSH P 1.)
(HLRZ@ 1. -4. P)
(CALL 1. (E CADR))
(CALL 2. (E CONS))
(MOVE 2. -2. P)
(CALL 2. (E CONS))
(MOVE 3. 1.)
(MOVE 2. -3. P)
(HRRZ@ 1. -4. P)
(HLRZ@ 1. 1.)
(CALL 3. (E BOUNDSUBST))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
TAG3 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP BOUNDSUBSTL SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(JUMPE 1. TAG1)
(MOVE 3. 0. P)
(MOVE 2. -1. P)
(HLRZ@ 1. -2. P)
(CALL 3. (E BOUNDSUBST))
(MOVE 3. 0. P)
(MOVE 2. -1. P)
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(CALL 3. (E BOUNDSUBSTL))
(POP P 2.)
(CALL 2. (E XCONS))
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP CONJOIN SUBR)
(PUSH P 1.)
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE TRUE))
(JRST 0. TAG1)
TAG2 (HRRZ@ 1. 1.)
(JUMPN 1. TAG4)
(HLRZ@ 1. 0. P)
(JRST 0. TAG1)
TAG4 (MOVE 2. 0. P)
(MOVEI 1. (QUOTE AND))
(CALL 2. (E CONS))
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP CURCOL SUBR)
(MOVEI 1. (QUOTE NIL))
(CALL 1. (E LINELENGTH))
(PUSH P 1.)
(CALL 0. (E CHRCT))
(MOVE 2. 1.)
(MOVEI 1. (QUOTE 1.))
(CALL 2. (E *DIF))
(POP P 2.)
(JCALL 2. (E *PLUS))
NIL
(LAP CURLINE SUBR)
(CALL 0. (E CURPROOF))
(MOVE 1. (SPECIAL CURLIN))
(POPJ P)
NIL
(LAP CURPROOF SUBR)
(MOVE 1. (SPECIAL CURPRF))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE (NO CURRENT PROOF)))
(CALL 1. (E ERREND))
(JRST 0. TAG1)
TAG2 (MOVE 1. (SPECIAL CURPRF))
TAG1 (POPJ P)
NIL
(LAP CURTEXT SUBR)
(CALL 0. (E CURPROOF))
(MOVEI 2. (QUOTE PROOF))
(JCALL 2. (E GET))
NIL
(LAP DOUBLENEG SUBR)
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (NOT (NOT PPP))))
(CALL 3. (E INST))
(PUSH P 1.)
(CALL 1. (E VALID))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG2 (MOVEI 2. (QUOTE PPP))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP EXGEN1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
TAG1 (MOVE 1. 0. P)
(JUMPN 1. TAG9)
(MOVE 1. -1. P)
(JRST 0. TAG5)
TAG9 (HLRZ@ 1. 0. P)
(CALL 1. (E ATOM))
(JUMPN 1. TAG2)
(MOVEI 2. (QUOTE CONS))
(HLRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPN 1. TAG3)
(MOVEI 1. (QUOTE (ILLEGAL ARGUMENT)))
(CALL 1. (E ERREND))
TAG2 (HLRZ@ 3. 0. P)
(MOVE 2. 3.)
(MOVE 1. -1. P)
(CALL 3. (E EXGEN))
(MOVEM 1. -1. P)
(JRST 0. TAG4)
TAG3 (HLRZ@ 3. 0. P)
(HRRZ@ 3. 3.)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(HLRZ@ 2. 0. P)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(MOVE 1. -1. P)
(CALL 3. (E EXGEN))
(MOVEM 1. -1. P)
TAG4 (HRRZ@ 1. 0. P)
(MOVEM 1. 0. P)
(JRST 0. TAG1)
TAG5 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP EXGEN SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(CALL 0. (E GENSYM))
(MOVE 3. -2. P)
(MOVE 2. -1. P)
(PUSH P 1.)
(CALL 3. (E SUBST))
(MOVEM 1. -3. P)
(CALL 1. (E ALLVARS))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG5)
(MOVEI 1. (QUOTE (NEW VARIABLE CONFLICTS)))
(CALL 1. (E ERREND))
TAG5 (MOVE 1. -1. P)
(CALL 1. (E NCONS))
(MOVEI 2. (QUOTE THEREEXISTS))
(CALL 2. (E XCONS))
(MOVE 3. -3. P)
(MOVE 2. 0. P)
(PUSH P 1.)
(MOVE 1. -2. P)
(CALL 3. (E SUBST))
(CALL 1. (E NCONS))
(POP P 2.)
(SUB P (C 0. 0. 4. 4.))
(JCALL 2. (E XCONS))
NIL
(LAP EQI1 SUBR)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES QQQ PPP)))
(CALL 3. (E INST))
(PUSH P 1.)
(CALL 1. (E VALID))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG2 (MOVEI 2. (QUOTE (EQUIVALENT PPP QQQ)))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ERREND SUBR)
(PUSH P 1.)
(CALL 1. (E PRINT))
(CALL 0. (E ERR))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP FREEIN SUBR)
(PUSH P 1.)
(PUSH P 2.)
(MOVE 1. 2.)
(JUMPE 1. TAG1)
(HLRZ@ 1. 1.)
(CALL 1. (E WFFPART))
(CALL 1. (E FREEVARS))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG2)
(MOVEI 1. (QUOTE T))
(JRST 0. TAG1)
TAG2 (HRRZ@ 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E FREEIN))
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP FREEVARS SUBR)
(MOVE 3. 1.)
(MOVEI 2. (QUOTE NIL))
(MOVEI 1. (QUOTE NIL))
(JCALL 3. (E FREEVARS1))
NIL
(LAP FREEVARS1 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(MOVE 1. 3.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. 3.)
(CALL 1. (E ISVAR))
(JUMPE 1. TAG4)
(MOVE 2. -2. P)
(MOVE 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG6)
(MOVE 1. -1. P)
(JRST 0. TAG5)
TAG6 (MOVE 2. -1. P)
(MOVE 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG7)
(MOVE 1. -1. P)
(JRST 0. TAG5)
TAG7 (MOVE 2. -1. P)
(MOVE 1. 0. P)
(CALL 2. (E CONS))
TAG5 (JRST 0. TAG3)
TAG4 (MOVE 1. -1. P)
TAG3 (JRST 0. TAG1)
TAG2 (HLRZ@ 1. 3.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG12)
(HRRZ@ 3. 3.)
(MOVE 1. -2. P)
(CALL 3. (E FREEVARS2))
(JRST 0. TAG1)
TAG12 (HLRZ@ 1. 3.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG13)
(MOVEI 2. (QUOTE (FORALL THEREEXISTS)))
(HLRZ@ 1. 3.)
(HLRZ@ 1. 1.)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG15)
(MOVE 2. -2. P)
(HLRZ@ 1. 0. P)
(CALL 1. (E CADR))
(CALL 2. (E CONS))
(HRRZ@ 3. 0. P)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(MOVE 2. -1. P)
(CALL 3. (E FREEVARS1))
TAG15 (JRST 0. TAG1)
TAG13 (MOVEI 1. (QUOTE (UNKNOWN NONATOMIC FUNCTION)))
(CALL 1. (E ERREND))
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP FREEVARS2 SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(JUMPN 3. TAG2)
(MOVE 1. 2.)
(JRST 0. TAG1)
TAG2 (HRRZ@ 3. 0. P)
(MOVE 2. -1. P)
(MOVE 1. -2. P)
(CALL 3. (E FREEVARS2))
(HLRZ@ 3. 0. P)
(MOVE 2. 1.)
(MOVE 1. -2. P)
(CALL 3. (E FREEVARS1))
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP GETCURLINE SUBR)
(CALL 0. (E CURLINE))
(JCALL 1. (E GETLINE))
NIL
(LAP GETLINE SUBR)
(PUSH P 1.)
(CALL 0. (E CURTEXT))
(MOVE 2. 1.)
(MOVE 1. 0. P)
(CALL 2. (E ASSOC))
(PUSH P 1.)
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NO SUCH LINE)))
(CALL 1. (E ERREND))
TAG5 (MOVE 1. 0. P)
(SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP GIVEPROOF FSUBR)
(PUSH P 1.)
(HLRZ@ 1. 1.)
(CALL 1. (E ATOM))
(JUMPN 1. TAG5)
(MOVEI 1. (QUOTE (NON ATOMIC PROOF NAME)))
(CALL 1. (E ERREND))
TAG5 (MOVE 2. (SPECIAL PROOFS))
(HLRZ@ 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG8)
(HLRZ@ 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. (SPECIAL PROOFS))
(CALL 2. (E *APPEND))
(MOVEM 1. (SPECIAL PROOFS))
TAG8 (MOVEI 3. (QUOTE PROOF))
(HRRZ@ 2. 0. P)
(HLRZ@ 2. 2.)
(HLRZ@ 1. 0. P)
(CALL 3. (E PUTPROP))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP IFE1 SUBR)
(PUSH P 2.)
(PUSH P 1.)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (PPP COND (PPP QQQ) (T RRR))))
(CALL 3. (E INST))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((NOT PPP) COND (PPP QQQ) (T RRR))))
(CALL 3. (E INST))
(MOVE 2. -1. P)
(PUSH P 1.)
(MOVE 1. -3. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE (PPP COND (PPP QQQ) (T RRR))))
(CALL 3. (E INST))
(MOVE 2. -2. P)
(EXCH 1. -3. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((NOT PPP) COND (PPP QQQ) (T RRR))))
(CALL 3. (E INST))
(MOVEM 1. -2. P)
(MOVE 1. -1. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG2)
(MOVEI 2. (QUOTE QQQ))
(MOVE 1. -1. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG2 (MOVE 1. 0. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG3)
(MOVEI 2. (QUOTE RRR))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG3 (MOVE 1. -3. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG4)
(MOVEI 2. (QUOTE QQQ))
(MOVE 1. -3. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG4 (MOVE 1. -2. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG5)
(MOVEI 2. (QUOTE RRR))
(MOVE 1. -2. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG5 (MOVEI 1. (QUOTE INVALID))
TAG1 (SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP IFI1 SUBR)
(PUSH P 2.)
(PUSH P 1.)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR)))
(CALL 3. (E INST))
(POP P 2.)
(EXCH 1. 0. P)
(CALL 2. (E CONS))
(MOVEI 3. (QUOTE NIL))
(MOVEI 2. (QUOTE ((IMPLIES PPP QQQ) IMPLIES (NOT PPP) RRR)))
(CALL 3. (E INST))
(PUSH P 1.)
(MOVE 1. -1. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG2)
(MOVEI 2. (QUOTE (COND (PPP QQQ) (T RRR))))
(MOVE 1. -1. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG2 (MOVE 1. 0. P)
(CALL 1. (E VALID))
(JUMPE 1. TAG3)
(MOVEI 2. (QUOTE (COND (PPP QQQ) (T RRR))))
(MOVE 1. 0. P)
(CALL 2. (E SUBLIS))
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE INVALID))
TAG1 (SUB P (C 0. 0. 2. 2.))
(POPJ P)
NIL
(LAP INITALL SUBR)
(CLEARM 0. (SPECIAL CURPRF))
(CLEARM 0. (SPECIAL AXIOMS))
(CLEARM 0. (SPECIAL THEOREMS))
(CLEARM 0. (SPECIAL PROOFS))
(CLEARM 0. (SPECIAL SCHEMAS))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP INITOPS SUBR)
(MOVE 2. (SPECIAL PRECLIS*))
(MOVEI 1. (QUOTE SETQ))
(CALL 2. (E CONS))
(MOVEI 2. (QUOTE *COMMA*))
(CALL 2. (E XCONS))
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -3. P)
(JUMPE 1. TAG3)
(HLRZ@ 1. -3. P)
(MOVEI 2. (QUOTE INFIX))
(MOVEM 1. -1. P)
(CALL 2. (E GET))
(MOVEM 1. -2. P)
(MOVEI 2. (QUOTE LEFT))
(MOVE 1. -1. P)
(CALL 2. (E GET))
(JUMPE 1. TAG8)
(MOVEI 1. (QUOTE 1.))
(CALL 1. (E MINUS))
(MOVE 2. 1.)
(JRST 0. TAG7)
TAG8 (MOVEI 2. (QUOTE 1.))
TAG7 (MOVEM 2. 0. P)
(MOVE 2. -2. P)
(MOVEI 1. (QUOTE 3.))
(CALL 2. (E *TIMES))
(MOVE 2. 0. P)
(CALL 2. (E *PLUS))
(MOVE 2. -2. P)
(PUSH P 1.)
(MOVEI 1. (QUOTE 3.))
(CALL 2. (E *TIMES))
(MOVE 2. -1. P)
(CALL 2. (E *DIF))
(CALL 1. (E NCONS))
(POP P 2.)
(CALL 2. (E XCONS))
(MOVEI 3. (QUOTE PREC))
(MOVE 2. 1.)
(MOVE 1. -1. P)
(CALL 3. (E PUTPROP))
(HRRZ@ 1. -3. P)
(MOVEM 1. -3. P)
(JRST 0. TAG1)
TAG3 (MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 4. 4.))
(POPJ P)
NIL
(LAP INITPROOF SUBR)
(PUSH P 1.)
(JUMPN 1. TAG6)
(MOVEI 1. (QUOTE (NIL NOT ACCEPTABLE PROOF NAME)))
(CALL 1. (E ERREND))
TAG6 (MOVE 1. 0. P)
(MOVEM 1. (SPECIAL CURPRF))
(MOVEI 2. (QUOTE (PROOF)))
(MOVE 1. 0. P)
(CALL 2. (E GETL))
(JUMPN 1. TAG1)
(MOVEI 3. (QUOTE PROOF))
(MOVEI 2. (QUOTE NIL))
(MOVE 1. 0. P)
(CALL 3. (E PUTPROP))
(MOVE 1. 0. P)
(CALL 1. (E NCONS))
(MOVE 2. 1.)
(MOVE 1. (SPECIAL PROOFS))
(CALL 2. (E *APPEND))
(MOVEM 1. (SPECIAL PROOFS))
TAG1 (CALL 0. (E CURTEXT))
(JUMPN 1. TAG10)
(MOVEI 1. (QUOTE 0.))
(JRST 0. TAG9)
TAG10 (CALL 0. (E CURTEXT))
(CALL 1. (E LAST))
(CALL 1. (E CAAR))
TAG9 (MOVEM 1. (SPECIAL CURLIN))
(CALL 0. (E CURLINE))
(MOVEI 3. (QUOTE NEWNAM))
(MOVE 2. 1.)
(MOVEI 1. (QUOTE /@))
(CALL 3. (E PUTPROP))
(MOVEI 1. (QUOTE NIL))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP INITSTANCHARSET SUBR)
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∧))
(MOVEI 1. (QUOTE AND))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE →→))
(MOVEI 1. (QUOTE CMAPS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /,))
(MOVEI 1. (QUOTE *COMMA*))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /.))
(MOVEI 1. (QUOTE CONS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ⊂))
(MOVEI 1. (QUOTE CONTAINED))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE DIFFERENCE))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE =))
(MOVEI 1. (QUOTE EQUAL))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ≡))
(MOVEI 1. (QUOTE EQUIVALENT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ↑))
(MOVEI 1. (QUOTE EXPT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∀))
(MOVEI 1. (QUOTE FORALL))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ≥))
(MOVEI 1. (QUOTE GEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE >))
(MOVEI 1. (QUOTE GREATERP))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ⊃))
(MOVEI 1. (QUOTE IMPLIES))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∩))
(MOVEI 1. (QUOTE INTERSECTION))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE λ))
(MOVEI 1. (QUOTE LAMBDA))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ≤))
(MOVEI 1. (QUOTE LEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE <))
(MOVEI 1. (QUOTE LESSP))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE →))
(MOVEI 1. (QUOTE MAPS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ε))
(MOVEI 1. (QUOTE MEMBER))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE MINUS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ≠))
(MOVEI 1. (QUOTE NEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ¬))
(MOVEI 1. (QUOTE NOT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∨))
(MOVEI 1. (QUOTE OR))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /+))
(MOVEI 1. (QUOTE PLUS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ⊗))
(MOVEI 1. (QUOTE PRODUCT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE '))
(MOVEI 1. (QUOTE QUOTE))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE //))
(MOVEI 1. (QUOTE QUOTIENT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ←))
(MOVEI 1. (QUOTE SETQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∃))
(MOVEI 1. (QUOTE THEREEXISTS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE *))
(MOVEI 1. (QUOTE TIMES))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ∪))
(MOVEI 1. (QUOTE UNION))
(CALL 3. (E PUTPROP))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP INITTTYCHARSET SUBR)
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE &))
(MOVEI 1. (QUOTE AND))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / CMAPS/ ))
(MOVEI 1. (QUOTE CMAPS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /,))
(MOVEI 1. (QUOTE *COMMA*))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /.))
(MOVEI 1. (QUOTE CONS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / CONT/ ))
(MOVEI 1. (QUOTE CONTAINED))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE DIFFERENCE))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE =))
(MOVEI 1. (QUOTE EQUAL))
(CALL 3. (E PUTPROP))
(MOVE 2. (SPECIAL GREATERP))
(MOVEI 1. (QUOTE <))
(CALL 2. (E EQUAL))
(MOVEI 3. (QUOTE INFXNAM))
(MOVE 2. 1.)
(MOVEI 1. (QUOTE EQUIVALENT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ↑))
(MOVEI 1. (QUOTE EXPT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE A))
(MOVEI 1. (QUOTE FORALL))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE >=))
(MOVEI 1. (QUOTE GEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE >))
(MOVEI 1. (QUOTE GREATERP))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE =>))
(MOVEI 1. (QUOTE IMPLIES))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / INTERSECT/ ))
(MOVEI 1. (QUOTE INTERSECTION))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE L))
(MOVEI 1. (QUOTE LAMBDA))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE <=))
(MOVEI 1. (QUOTE LEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE <))
(MOVEI 1. (QUOTE LESSP))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / MAPS/ ))
(MOVEI 1. (QUOTE MAPS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / MEMBER/ ))
(MOVEI 1. (QUOTE MEMBER))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE MINUS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / NEQ/ ))
(MOVEI 1. (QUOTE NEQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /-))
(MOVEI 1. (QUOTE NOT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / V/ ))
(MOVEI 1. (QUOTE OR))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE /+))
(MOVEI 1. (QUOTE PLUS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / PROD/ ))
(MOVEI 1. (QUOTE PRODUCT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE '))
(MOVEI 1. (QUOTE QUOTE))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE //))
(MOVEI 1. (QUOTE QUOTIENT))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE ←))
(MOVEI 1. (QUOTE SETQ))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE E))
(MOVEI 1. (QUOTE THEREEXISTS))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE *))
(MOVEI 1. (QUOTE TIMES))
(CALL 3. (E PUTPROP))
(MOVEI 3. (QUOTE INFXNAM))
(MOVEI 2. (QUOTE / UNION/ ))
(MOVEI 1. (QUOTE UNION))
(CALL 3. (E PUTPROP))
(MOVEI 1. (QUOTE NIL))
(POPJ P)
NIL
(LAP INST SUBR)
(PUSH P 1.)
(PUSH P 2.)
(PUSH P 3.)
(MOVE 1. 3.)
(CALL 1. (E VALID))
(JUMPN 1. TAG2)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG2 (MOVE 1. -1. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG4)
(MOVEI 2. (QUOTE (PPP QQQ RRR SSS)))
(MOVE 1. -1. P)
(CALL 2. (E MEMBER))
(JUMPE 1. TAG6)
(MOVE 2. 0. P)
(MOVE 1. -1. P)
(CALL 2. (E ASSOC))
(PUSH P 1.)
(JUMPN 1. TAG8)
(MOVE 2. -3. P)
(MOVE 1. -2. P)
(CALL 2. (E CONS))
(MOVE 2. -1. P)
(CALL 2. (E CONS))
(JRST 0. TAG7)
TAG8 (MOVE 2. -3. P)
(HRRZ@ 1. 1.)
(CALL 2. (E EQUAL))
(JUMPE 1. TAG10)
(MOVE 1. -1. P)
(JRST 0. TAG7)
TAG10 (MOVEI 1. (QUOTE INVALID))
TAG7 (SUB P (C 0. 0. 1. 1.))
(JRST 0. TAG5)
TAG6 (MOVE 1. -1. P)
(CAME 1. -2. P)
(JRST 0. TAG13)
(MOVE 1. 0. P)
(JRST 0. TAG5)
TAG13 (MOVEI 1. (QUOTE INVALID))
TAG5 (JRST 0. TAG1)
TAG4 (MOVE 1. -2. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG16)
(MOVEI 1. (QUOTE INVALID))
(JRST 0. TAG1)
TAG16 (HRRZ@ 1. -1. P)
(PUSH P 1.)
(HRRZ@ 1. -3. P)
(MOVE 3. -1. P)
(HLRZ@ 2. -2. P)
(PUSH P 1.)
(HLRZ@ 1. -4. P)
(CALL 3. (E INST))
(MOVE 3. 1.)
(MOVE 2. -1. P)
(POP P 1.)
(CALL 3. (E INST))
(SUB P (C 0. 0. 1. 1.))
TAG1 (SUB P (C 0. 0. 3. 3.))
(POPJ P)
NIL
(LAP ISCONST SUBR)
(PUSH P 1.)
(CALL 1. (E NUMBERP))
(JUMPN 1. TAG1)
(MOVE 2. (SPECIAL LOGICALCONSTANTS))
(MOVE 1. 0. P)
(CALL 2. (E MEMBER))
(JUMPN 1. TAG1)
(TDZA 1. 1.)
TAG1 (MOVEI 1. (QUOTE T))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ISEQUIVALENCE SUBR)
(MOVEI 2. (QUOTE (EQUAL EQUIVALENT SETQ)))
(JCALL 2. (E MEMBER))
NIL
(LAP ISIDENT SUBR)
(PUSH P 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. 0. P)
(CALL 1. (E NUMBERP))
(JUMPE 1. TAG1)
TAG2 (TDZA 1. 1.)
TAG1 (MOVEI 1. (QUOTE T))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP ISQUANT SUBR)
(MOVE 2. (SPECIAL QUANTIFIERS))
(JCALL 2. (E MEMBER))
NIL
(LAP ISVAR SUBR)
(PUSH P 1.)
(CALL 1. (E ISIDENT))
(JUMPE 1. TAG2)
(MOVE 1. 0. P)
(CALL 1. (E ISCONST))
(JUMPE 1. TAG1)
TAG2 (TDZA 1. 1.)
TAG1 (MOVEI 1. (QUOTE T))
(SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP LAMEXP SUBR)
(PUSH P 1.)
(CALL 1. (E ATOM))
(JUMPE 1. TAG2)
(MOVE 1. 0. P)
(JRST 0. TAG1)
TAG2 (HLRZ@ 1. 0. P)
(CALL 1. (E ATOM))
(JUMPE 1. TAG3)
(HLRZ@ 1. 0. P)
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E LAMEXPL))
(POP P 2.)
(CALL 2. (E XCONS))
(JRST 0. TAG1)
TAG3 (MOVEI 2. (QUOTE LAMBDA))
(HLRZ@ 1. 0. P)
(CALL 1. (E CAAR))
(CALL 2. (E EQUAL))
(JUMPE 1. TAG4)
(HLRZ@ 3. 0. P)
(HRRZ@ 3. 3.)
(HLRZ@ 3. 3.)
(HLRZ@ 2. 0. P)
(HLRZ@ 2. 2.)
(HRRZ@ 2. 2.)
(HLRZ@ 2. 2.)
(HRRZ@ 1. 0. P)
(HLRZ@ 1. 1.)
(CALL 3. (E PROPSUBST))
(JRST 0. TAG1)
TAG4 (HLRZ@ 1. 0. P)
(CALL 1. (E LAMEXP))
(PUSH P 1.)
(HRRZ@ 1. -1. P)
(CALL 1. (E LAMEXPL))
(POP P 2.)
(CALL 2. (E XCONS))
TAG1 (SUB P (C 0. 0. 1. 1.))
(POPJ P)
NIL
(LAP LAMEXPL SUBR)
(MOVE 2. 1.)
(MOVEI 1. (QUOTE LAMEXP))
(JCALL 2. (E MAPCAR))
NIL
(LAP MAKECONSES SUBR)
(PUSH P 1.)
(PUSH P (C 0. 0. (QUOTE NIL) 0.))
TAG1 (MOVE 1. -1. P)